
\begin{frame}
\frametitle{Temporale Logiken}
Temporale Logiken erweitern die Aussagenlogik um zeitliche Abläufe
\begin{columns}
\column{.58\textwidth}
\begin{itemize}
\item Linear Time
\begin{itemize}
\item Beschreibung einer Folge von Zuständen
\item \emph{Linear Temporal Logic} (LTL)
\end{itemize}
\end{itemize}
\column{.38\textwidth}
\begin{center}	
	\begin{tikzpicture}[auto]
	\node [draw, circle] (a) at (0,0) {\tiny 1};
	\node [draw, circle] (b) at (1,0) {\tiny 2};
	\node [draw, circle] (c) at (2,0) {\tiny 3};

	\draw (a) [->,thick] to node {} (b);
	\draw (b) [->,thick] to node {} (c);
	\end{tikzpicture}
	\end{center}
\end{columns}
\begin{columns}
\column{.58\textwidth}
\begin{itemize}
\item Branching Time
\begin{itemize}
\item Mehrere Folgezustände sind mögliche
\item \emph{Computation Tree Logic} (CTL)
\end{itemize}
\end{itemize}
\column{.38\textwidth}
\begin{center}	
	\begin{tikzpicture}[auto]
	\node [draw, circle] (a) at (0,0) {\tiny 1};
	\node [draw, circle] (b) at (1,0.5) {\tiny 2};
	\node [draw, circle] (c) at (1,-0.5) {\tiny 3};

	\draw (a) [->,thick] to node {} (b);
	\draw (a) [->,thick] to node {} (c);
	\end{tikzpicture}
	\end{center}
\end{columns}
%\begin{itemize}
%\item Die \emph{Computation Tree Logic} (CTL) ist eine Temporale Logik basierend auf Baumstrukturen
%\item Aussagen über den Verlauf eines Systems können als Formel in CTL ausgedrückt werden
%\item Ein Model-Checker überprüft, ob die Formel in einem System erfüllt ist
%\end{itemize}
\end{frame}

\subsection*{CTL Syntax}
\begin{frame}
\frametitle{Aufbau von Formeln in CTL}
\begin{block}{Definition: CTL Syntax}
\vspace*{-0.5cm}
\begin{eqnarray}
 \varphi &::=& \pause \top \mid \bot \mid p \mid \lnot \varphi \mid \varphi \land \varphi \mid \varphi \lor \varphi \mid \varphi \Rightarrow \varphi \mid \varphi \Leftrightarrow \varphi      \nonumber \\
   & & \pause \mathsf{AX} \; \varphi \mid \mathsf{EX} \; \varphi \mid \mathsf{AF} \; \varphi \mid \mathsf{EF} \; \varphi \mid \mathsf{AG} \; \varphi \mid \mathsf{EG} \; \varphi \nonumber \\
    & & \pause \mathsf{A} \; [\varphi \mathop{\mathsf{U}} \varphi] \mid \mathsf{E} \; [\varphi \mathop{\mathsf{U}} \varphi] \nonumber
\end{eqnarray}
\end{block}
\pause 
\begin{exampleblock}{Beispielformeln}
\begin{itemize}
\item $\varphi \triangleq (p \Rightarrow q) \Leftrightarrow (\lnot q \Rightarrow \lnot p)$
\item $\varphi \triangleq \mathsf{AX} \; \mathsf{EF} \; p$
\item $\varphi \triangleq \mathsf{A} \; [\mathsf{EX} \; p \mathop{\mathsf{U}} q] \Rightarrow \lnot q$
\end{itemize}
\end{exampleblock}
\end{frame}

\subsection*{CTL Semantik}
\begin{frame}
\frametitle{Bedeutung von Formeln in CTL}
\begin{columns}
\column{.58\textwidth}

\begin{block}{Definition: CTL Semantik}
Pfadquantoren:
\begin{itemize}
\item $\mathsf{A}$ : Auf allen folgenden Pfaden
\item $\mathsf{E}$ : Auf mindestens einem Pfad
\end{itemize}
Temporaloperatoren:
\begin{itemize}
\item $\mathsf{X} \; \varphi$ : Im nächsten Zustand
\item $\mathsf{F} \; \varphi$ : In einem folgenden Zustand
\item $\mathsf{G} \; \varphi$ : In allen folgenden Zuständen
\item $\left[ \varphi \mathop{\mathsf{U}} \psi \right]$ : Es gilt $\varphi$ bis zum ersten Auftreten von $\psi$
\end{itemize}
\end{block}
\column{.38\textwidth}
\begin{center}	
Aufbau einer CTL Formel:

\vspace*{1cm}
	\begin{tikzpicture}[auto]
	\node  (a) at (-0.5,0) {\Huge $\mathbf{Q}$};
	\node  (b) at (.5,0.03) {\Huge $\mathbf{T}$};
	\node  (c) at (-.5,1) {\small Pfadquantor};
	\node  (d) at (.5,-1) {\small Temporaloperator};

	%\draw (a) [->,thick] to node {} (c);
	%\draw (b) [->,thick] to node {} (c);
	\draw (c) [->,thick] to node {} (a);
	\draw (d) [->,thick] to node {} (b);
	%\draw (d) [->,bend left,dashed,color=red] to node {} (a);
		
	\end{tikzpicture}
	\end{center}
	
\vspace*{1cm}

\end{columns}
\end{frame}

\begin{frame}
\frametitle{CTL Erfüllbarkeit}
\begin{columns}
\column{.48\textwidth}
\begin{block}{Definition: Erfüllbarkeit in CTL}
Erfüllt eine Systembeschreibung\footnote{Typischerweise eine Kripke-Struktur} $\mathcal{M}$ in einem Zustand $\mathsf{S}$ eine CTL Formel $\varphi$, so schreiben wir: $$\mathcal{M},\mathsf{S} \vDash \varphi$$

Ist $\mathsf{S}$ ein initialer Zustand, schreiben wir: $$\mathcal{M} \vDash \varphi$$
\end{block}
\column{.48\textwidth}
Beispiel: $\varphi \triangleq \mathsf{EG} \; p$\\mit $\mathcal{M}:$
\vspace*{0.1cm} 
\begin{center}	
	\begin{tikzpicture}[auto]
	\node [circle, draw, minimum height=1cm] (a) at (0,0) {$p$};
	\node [circle, draw, minimum height=1cm] (b) at (-1,-1.5) {$p$};
	\node [circle, draw, minimum height=1cm] (c) at (1,-1.5) {};
	\node [circle, draw, minimum height=1cm] (d) at (-2,-3) {};
	\node [circle, draw, minimum height=1cm] (e) at (-0.5,-3) {$p$};
	\node [circle, draw, minimum height=1cm] (f) at (1,-3) {};

	\draw (a) [->,thick] to node {} (b);
	\draw (a) [->,thick] to node {} (c);
	\draw (b) [->,thick] to node {} (d);
	\draw (b) [->,thick] to node {} (e);
	\draw (c) [->,thick] to node {} (f);
		
	\end{tikzpicture}
	\end{center}
\end{columns}

\end{frame}

%TODO Noch eine Folie mit den Beispielen die wir an der Tafel benutzen.


\begin{frame}
\frametitle{Computational Tree Logic (CTL)}
\begin{columns}
\column{.66\textwidth}
\begin{exampleblock}{Aufgabe: $\mathcal{M} \vDash \varphi_1$?}
Erfüllt das Modell $\mathcal{M}$ die Spezifikation $\varphi_1$ ?
$$\varphi_1 \triangleq (\mathsf{AF} \; p) \land (\mathsf{EX} \; q) $$
\end{exampleblock}
\onslide<2->{
\begin{exampleblock}{Aufgabe: $\mathcal{M} \vDash \varphi_2$?}
Erfüllt das Modell $\mathcal{M}$ die Spezifikation $\varphi_2$ ?
$$\varphi_2 \triangleq \mathsf{E} \left[ p \operatorname{\mathsf{U}} q\right]$$
\end{exampleblock}}
\onslide<3->{
\begin{exampleblock}{Aufgabe: $\mathcal{M} \vDash \varphi_3$ !}
Finde eine Formel $\varphi_3$ die in $\mathcal{M}$ erfüllt ist!
}
\onslide<4->{
$$\text{Lösung: } \varphi_3 \triangleq \mathsf{AF} ( p \Rightarrow (\mathsf{AX} q ))$$
\end{exampleblock}
}
\column{.30\textwidth}
\vspace*{2cm}
\begin{center}
$\mathcal{M}$ siehe Tafel $\rightsquigarrow$
\end{center}
\end{columns}
\end{frame}